import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.Formula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import proof.Proof;
import proof.ProofRule;
import proof.DerivedProof;
import sign.FormulaSign;

import java.util.ArrayList;

public class test {

    public static void main(String[] args) {
        //f1 ANY(q,l)
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,q,l);
        //f2 Exist(p,q)
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        //Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        BinaryFormula f2=new BinaryFormula(FormulaSign.EXIST,p,q);

        //not p
        UnaryFormula not_p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),true));

        System.out.println(f1);
        System.out.println(f2);
        //System.out.println(not_p);

        Proof p1=new ConclusionProof(f1);
        Proof p2=new ConclusionProof(f2);
        ArrayList<Proof> ps=new ArrayList<>();
        ps.add(p1);
        ps.add(p2);
        Formula conclusion=ProofRule.D1.applyRule(ps);
        Proof res=new DerivedProof(ps,ProofRule.D1);

        // step 1
        System.out.println(res);  // ∀(q,l),∃(p,q)->∃(p,l)
        System.out.println(Solve.solveHelper(ps, conclusion, new UsedCondition())); // [{ANY(q,l),Exist(p,q)}D1 -> Exist(p,l)]

        // step 2  [∀(q,l),∃(p,q)->∃(p,l)], ∃(r,l) -> ∃(r,p)
        // f3 ANY(l,r)
        UnaryFormula r=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r"),false));
        BinaryFormula f3=new BinaryFormula(FormulaSign.ANY,l,r);
        Proof p3 = new ConclusionProof(f3);

        ArrayList<Proof> ps2=new ArrayList<>();
        ps2.add(p3);
        ps2.add(res);// ∀(q,l),∃(p,q)->∃(p,l)
        //此时ps2：ANY(l.r)，∀(q,l),∃(p,q)->∃(p,l)
        Formula conclusion2=ProofRule.D1.applyRule(ps2);
        Proof res2=new DerivedProof(ps2,ProofRule.D1);
        System.out.println(res2);//[{ANY(l,r),[{ANY(q,l),Exist(p,q)}D1 -> Exist(p,l)]}D1 -> Exist(p,r)]

        ps=new ArrayList<>();
        ps.add(p1);
        ps.add(p2);
        ps.add(p3);
        System.out.println(Solve.solveHelper(ps,conclusion2, new UsedCondition()));
        // [{ANY(l,r),[{ANY(q,l),Exist(p,q)}D1 -> Exist(p,l)]}D1 -> Exist(p,r)]

       // System.out.println(new Rule_Formula().D1F(f1,f2));


    }
}





